|
|
Dependability Assessment of Fault Tolerant Systems
Suchánek, Martin ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
Reliability is an important part of various systems. The aim of the work is to create reliability models of some reconfigurable and nonreconfigurable fault tolerant systems and subsequent evaluation of their reliability indicators. The Uppaal tool is used to create models, along with the SMC extension, which is used for verification. The result of the work is the verification of models and evaluation of reliability indicators using the tool Uppaal SMC.
|
|
|
Conversion of XTR Output of UPPAAL Tool into User-Friendly Representation
Mazánek, Antonín ; Mrázek, Vojtěch (referee) ; Strnadel, Josef (advisor)
The master's thesis introduces the Uppaal tool. It describes the principles and possibilities of modeling and analysis of systems using this tool. It also discusses in more detail the file formats that Uppaal tool uses. The structure of the XML file used to store created systems, the XTR format, which Uppaal uses to store simulation traces, and the IF format, which is necessary to understand the contents of the file in XTR format. The text also mentions available software support for working with these formats. Next part of this master's thesis is about designing user-friendly representation of simulations traces, along with designing application that translates simulation traces into designed representation. At the end of this thesis, the possible continuation of the project is mentioned together with the evaluation of the designed representation and the application.
|
|
|
ESP/ESC Impact to Behavior of Vehicle
Weigel, Filip ; Mrázek, Vojtěch (referee) ; Strnadel, Josef (advisor)
This bachelor thesis focuses on active safety - ESP. System ESP greatly improves stability of vehicle while turning. The thesis analyses modelling, brake functionality, subordinate systems of ESP - ABS and ASR, physical forces and phenomenons, model example, analysis of problem, design of model, implementation of model and experiments evaluation of implemented model in UPPAAL enviroment. The goal of the thesis is to prove that ESP system helps to stabilize vehicle while turning by simulation of vehicle model. Results are presented in well-aranged graphs side-by-side. It is possible to analyze the behaviour of vehicle while turning with ESP or without ESP.
|
|
| |
|
|
System for Guarding and Securing Objects and Areas
Kuchařík, David ; Kubek, Ján (referee) ; Strnadel, Josef (advisor)
This project deals with given safeguard possibilities, both mechanical and electronic. A row house with garden was chosen for being secured. Subsequently, were elaborated two`s proposals of securing and guarding of this object. First, was based on camera`s system and second on common system ESS. Later on they were evaluated and the most considerable benefits were emphasized. A system based on control panel with connected detectors was selected upon specification. Subsequently was created a model of the chosen system, at which the required behaviour was simulated and verified. An outline of an implementation was created in the C language.
|
|
|
Computational Model and Analysis of Adaptive Traffic Lights
Terbr, Filip ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
This thesis deals with the topic of adaptive intersections and the study of their influence on the flow of traffic and others. The work contains an analysis of currently used traffic detectors, an analysis of the main problems of classic intersections and the possibilities of their solution, followed by the design of the model, a description of the implementation and testing of the created model. The resulting model is created in the UPPAAL SMC software and is a system of timed automata communicating with each other. Testing is performed by comparing the results of tests of classical traffic lights with the results of adaptive traffic lights.
|
|
|
Computational Model and Analysis of Energy-Aware Buildings
Kaleta, Radoslav ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
The thesis deals with the analysis of the properties of the external and internal environment of the buildings, the possibilities of heating and cooling. The emphasis is mainly on the energy intensity and the impact of weather conditions on the building temperature during the year. The model created by UPPAAL SMC describes the behavior of heating and cooling during the year and identifies the energy demand of the given building. The building model itself can be partially modified using the built-in user interface.
|
|
|
Modeling and Analysis of Self-Parking Vehicle Control
Krucina, Marek ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
This bachelor thesis deals with self-parking vehicles and their behavior. It describes the levels of parking automation and related technologies. It describes the kinematic model of the vehicle and various ways of representing movement. It summarizes the basic modeling tools and focuses mainly on the UPPAAL SMC tool, in which a model of a self-parking vehicle and its surroundings is subsequently created. Its implementation is described in the work. At the end of the work, the created model is analyzed by using the method of statistical model checking of the model and then examines the effect of traffic density.
|
|
|
Privacy Protection on Mobile Devives
Aron, Lukáš ; Hudec,, Ladislav (referee) ; Drahanský, Martin (referee) ; Hanáček, Petr (advisor)
Tato práce analyzuje ochranu citlivých dat na mobilních zařízeních a představuje metodu pro ochranu těchto dat před možností úniku informaci ze zařízení. Ochrana se zaměřuje na využívání zařízení, jak pro osobní účely, tak i v pracovním prostředí. Koncept navrženého řešení je implementován ve formě prototypu. Model implementace je verifikován s modelem požadovaného chování. Součástí práce jsou experimenty s prototypem a experimenty zaměřené na verifikaci mezi danými modely.
|
|
|
Risk Analysis of Self-Driven Vehicles
Weigel, Filip ; Šimek, Václav (referee) ; Strnadel, Josef (advisor)
The goal of this thesis was to design and implement system for risk analysis in self-driving cars. This thesis focused on design and implementation of system for risk analysis in models. One of the requirements for the system was to be flexible and robust. Design of the risk analysis was presented at theoretical level and then implemented in models of ABS and ESP systems in UPPAAL environment. The system was then tested via multiple experiments. The experiments were beneficial and the system for risk analysis correctly evaluated failure scenarios with adequate response to the rising level of risk. Experiment outputs were then presented at graphs with comment to each failure scenario.
|
guest ::
